Nuprl Lemma : mon_itop_unroll_unit
13,42
postcript
pdf
g
:IMonoid,
i
,
j
:
. (
i
+1 =
j
)
(
E
:({
i
..
j
}
|
g
|). (
i
k
<
j
.
E
(
k
)) =
E
(
i
))
latex
Up
groups
1
Definitions of Statement
lb
i
<
ub
.
E
(
i
)
Definitions
lb
i
<
ub
.
E
(
i
)
Lemmas
itop
unroll
unit
origin
g:IMonoid, i, j:
. (i+1 = j) 
(E:({i..j
}
|g|). (
i 
k < j. E(k)) = E(i)) g:IMonoid, i, j:. (i+1 = j) (E:({i..j}|g|). ( i k < j. E(k)) = E(i)) lb i < ub. E(i) lb i < ub. E(i)